YES 3.458
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((elemIndices :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> [Int]) :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (\vv1 ->
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\vv1→
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices0 | p vv1 | =
case | vv1 of | | (x,i) | → if p x then i : [] else [] |
| _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
| ((elemIndices :: (Eq a, Eq b) => (b,a) -> [(b,a)] -> [Int]) :: (Eq a, Eq b) => (b,a) -> [(b,a)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = |
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Case Reductions:
The following Case expression
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices00 | p (x,i) | = if p x then i : [] else [] |
findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
| ((elemIndices :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> [Int]) :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | if p x then i : [] else [] |
findIndices00 | p _ | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
findIndices000 | i True | = i : [] |
findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> [Int]) :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p _ | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((elemIndices :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> [Int]) :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule List
| ((elemIndices :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> [Int]) :: (Eq a, Eq b) => (b,a) -> [(b,a)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule List
| (elemIndices :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(yu3000), Succ(yu4110000)) → new_primEqNat(yu3000, yu4110000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yu10400), Succ(yu411001000)) → new_primPlusNat(yu10400, yu411001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yu10400), Succ(yu411001000)) → new_primPlusNat(yu10400, yu411001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yu30100), Succ(yu41100100)) → new_primMulNat(yu30100, Succ(yu41100100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yu30100), Succ(yu41100100)) → new_primMulNat(yu30100, Succ(yu41100100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(yu300, yu411000, bdh, bea)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], da), cc, cd) → new_esEs1(yu300, yu411000, da)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(yu302, yu411002, fh, ga)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_@2, bbd), bbe)) → new_esEs2(yu301, yu411001, bbd, bbe)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_@2, ed), ee), cd) → new_esEs2(yu301, yu411001, ed, ee)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_Maybe, bag)) → new_esEs(yu301, yu411001, bag)
new_esEs(Just(yu300), Just(yu411000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(yu300, yu411000, bb, bc, bd)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, hd), he) → new_esEs(yu300, yu411000, hd)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_[], ec), cd) → new_esEs1(yu301, yu411001, ec)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(yu300, yu411000, beb, bec)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), hc) → new_esEs1(yu301, yu411001, hc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bab), bac), he) → new_esEs2(yu300, yu411000, bab, bac)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], gf)) → new_esEs1(yu300, yu411000, gf)
new_esEs(Just(yu300), Just(yu411000), app(ty_Maybe, ba)) → new_esEs(yu300, yu411000, ba)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(yu301, yu411001, dh, ea, eb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, db), dc), cc, cd) → new_esEs2(yu300, yu411000, db, dc)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(yu300, yu411000, bdd, bde, bdf)
new_esEs3(Left(yu300), Left(yu411000), app(app(ty_Either, bch), bda), bca) → new_esEs3(yu300, yu411000, bch, bda)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], baa), he) → new_esEs1(yu300, yu411000, baa)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_[], fd)) → new_esEs1(yu302, yu411002, fd)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, ha), hb)) → new_esEs3(yu300, yu411000, ha, hb)
new_esEs3(Left(yu300), Left(yu411000), app(app(app(ty_@3, bcb), bcc), bcd), bca) → new_esEs0(yu300, yu411000, bcb, bcc, bcd)
new_esEs(Just(yu300), Just(yu411000), app(app(ty_@2, bf), bg)) → new_esEs2(yu300, yu411000, bf, bg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_@2, ff), fg)) → new_esEs2(yu302, yu411002, ff, fg)
new_esEs3(Left(yu300), Left(yu411000), app(app(ty_@2, bcf), bcg), bca) → new_esEs2(yu300, yu411000, bcf, bcg)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(yu301, yu411001, bah, bba, bbb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(yu302, yu411002, fa, fb, fc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_Either, bbf), bbg)) → new_esEs3(yu301, yu411001, bbf, bbg)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, gb)) → new_esEs(yu300, yu411000, gb)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_[], bdg)) → new_esEs1(yu300, yu411000, bdg)
new_esEs(Just(yu300), Just(yu411000), app(ty_[], be)) → new_esEs1(yu300, yu411000, be)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(yu300, yu411000, dd, de)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, hf), hg), hh), he) → new_esEs0(yu300, yu411000, hf, hg, hh)
new_esEs(Just(yu300), Just(yu411000), app(app(ty_Either, bh), ca)) → new_esEs3(yu300, yu411000, bh, ca)
new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_Maybe, bdc)) → new_esEs(yu300, yu411000, bdc)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, gc), gd), ge)) → new_esEs0(yu300, yu411000, gc, gd, ge)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_Maybe, dg), cd) → new_esEs(yu301, yu411001, dg)
new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, gg), gh)) → new_esEs2(yu300, yu411000, gg, gh)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_[], bbc)) → new_esEs1(yu301, yu411001, bbc)
new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bad), bae), he) → new_esEs3(yu300, yu411000, bad, bae)
new_esEs3(Left(yu300), Left(yu411000), app(ty_[], bce), bca) → new_esEs1(yu300, yu411000, bce)
new_esEs3(Left(yu300), Left(yu411000), app(ty_Maybe, bbh), bca) → new_esEs(yu300, yu411000, bbh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_Maybe, eh)) → new_esEs(yu302, yu411002, eh)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(yu301, yu411001, ef, eg)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, cb), cc, cd) → new_esEs(yu300, yu411000, cb)
new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(yu300, yu411000, ce, cf, cg)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_Either, ha), hb)) → new_esEs3(yu300, yu411000, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(app(ty_@3, gc), gd), ge)) → new_esEs0(yu300, yu411000, gc, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(app(ty_@2, gg), gh)) → new_esEs2(yu300, yu411000, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(yu300), Just(yu411000), app(app(ty_Either, bh), ca)) → new_esEs3(yu300, yu411000, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(yu300), Just(yu411000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(yu300, yu411000, bb, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(yu300), Just(yu411000), app(app(ty_@2, bf), bg)) → new_esEs2(yu300, yu411000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_Maybe, gb)) → new_esEs(yu300, yu411000, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(yu300), Just(yu411000), app(ty_Maybe, ba)) → new_esEs(yu300, yu411000, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(yu300), Just(yu411000), app(ty_[], be)) → new_esEs1(yu300, yu411000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_Either, bbf), bbg)) → new_esEs3(yu301, yu411001, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_Either, bad), bae), he) → new_esEs3(yu300, yu411000, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(yu301, yu411001, bah, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(app(ty_@3, hf), hg), hh), he) → new_esEs0(yu300, yu411000, hf, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(app(ty_@2, bbd), bbe)) → new_esEs2(yu301, yu411001, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(app(ty_@2, bab), bac), he) → new_esEs2(yu300, yu411000, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_Maybe, bag)) → new_esEs(yu301, yu411001, bag)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_Maybe, hd), he) → new_esEs(yu300, yu411000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), app(ty_[], baa), he) → new_esEs1(yu300, yu411000, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu411000, yu411001), baf, app(ty_[], bbc)) → new_esEs1(yu301, yu411001, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(yu300, yu411000, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(yu300), Left(yu411000), app(app(ty_Either, bch), bda), bca) → new_esEs3(yu300, yu411000, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(yu302, yu411002, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(yu300, yu411000, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(yu301, yu411001, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), hc) → new_esEs1(yu301, yu411001, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(yu300, yu301), :(yu411000, yu411001), app(ty_[], gf)) → new_esEs1(yu300, yu411000, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(yu300, yu411000, bdd, bde, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(Left(yu300), Left(yu411000), app(app(app(ty_@3, bcb), bcc), bcd), bca) → new_esEs0(yu300, yu411000, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(yu301, yu411001, dh, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(yu302, yu411002, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(yu300, yu411000, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Right(yu300), Right(yu411000), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(yu300, yu411000, bdh, bea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(yu300), Left(yu411000), app(app(ty_@2, bcf), bcg), bca) → new_esEs2(yu300, yu411000, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_Maybe, bdc)) → new_esEs(yu300, yu411000, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(yu300), Left(yu411000), app(ty_Maybe, bbh), bca) → new_esEs(yu300, yu411000, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(yu300), Right(yu411000), bdb, app(ty_[], bdg)) → new_esEs1(yu300, yu411000, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(yu300), Left(yu411000), app(ty_[], bce), bca) → new_esEs1(yu300, yu411000, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(app(ty_@2, ed), ee), cd) → new_esEs2(yu301, yu411001, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(app(ty_@2, db), dc), cc, cd) → new_esEs2(yu300, yu411000, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(app(ty_@2, ff), fg)) → new_esEs2(yu302, yu411002, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_Maybe, dg), cd) → new_esEs(yu301, yu411001, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_Maybe, eh)) → new_esEs(yu302, yu411002, eh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_Maybe, cb), cc, cd) → new_esEs(yu300, yu411000, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), app(ty_[], da), cc, cd) → new_esEs1(yu300, yu411000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, app(ty_[], ec), cd) → new_esEs1(yu301, yu411001, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), df, cc, app(ty_[], fd)) → new_esEs1(yu302, yu411002, fd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs(yu85, False, yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)
new_foldr(@2(yu30, yu31), @2(yu41100, yu41101), yu4111, yu61, yu62, bc, bd) → new_psPs(yu61, new_asAs(new_esEs4(yu30, yu41100, bc), new_esEs5(yu31, yu41101, bd)), yu30, yu31, yu4111, yu62, bc, bd)
new_psPs(yu85, True, yu87, yu88, yu89, yu90, ba, bb) → new_psPs0(yu87, yu88, yu89, yu90, ba, bb)
new_psPs0(yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)
The TRS R consists of the following rules:
new_esEs22(yu302, yu411002, ty_Integer) → new_esEs14(yu302, yu411002)
new_esEs7(Just(yu300), Just(yu411000), app(ty_Maybe, fd)) → new_esEs7(yu300, yu411000, fd)
new_esEs7(Just(yu300), Just(yu411000), app(ty_[], ga)) → new_esEs15(yu300, yu411000, ga)
new_esEs20(yu300, yu411000, app(ty_Maybe, gg)) → new_esEs7(yu300, yu411000, gg)
new_esEs25(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs22(yu302, yu411002, app(app(ty_@2, bbh), bca)) → new_esEs16(yu302, yu411002, bbh, bca)
new_esEs6(Left(yu300), Left(yu411000), app(app(ty_@2, cc), cd), bf) → new_esEs16(yu300, yu411000, cc, cd)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs27(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_primPlusNat1(Succ(yu10400), Succ(yu411001000)) → Succ(Succ(new_primPlusNat1(yu10400, yu411001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu411000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu411000)) → False
new_esEs7(Nothing, Just(yu411000), ed) → False
new_esEs7(Just(yu300), Nothing, ed) → False
new_esEs13(False, True) → False
new_esEs13(True, False) → False
new_esEs21(yu301, yu411001, ty_Ordering) → new_esEs12(yu301, yu411001)
new_esEs24(yu301, yu411001, app(app(ty_@2, bff), bfg)) → new_esEs16(yu301, yu411001, bff, bfg)
new_esEs27(yu300, yu411000, app(ty_Ratio, bhb)) → new_esEs18(yu300, yu411000, bhb)
new_esEs10(Char(yu300), Char(yu411000)) → new_primEqNat0(yu300, yu411000)
new_primEqInt(Pos(Zero), Neg(Succ(yu4110000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu4110000))) → False
new_esEs21(yu301, yu411001, ty_@0) → new_esEs19(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Ordering) → new_esEs12(yu301, yu411001)
new_esEs27(yu300, yu411000, app(ty_Maybe, bgc)) → new_esEs7(yu300, yu411000, bgc)
new_esEs23(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_@0) → new_esEs19(yu31, yu41101)
new_esEs6(Left(yu300), Left(yu411000), app(ty_[], cb), bf) → new_esEs15(yu300, yu411000, cb)
new_esEs23(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Double) → new_esEs9(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), app(app(ty_Either, ge), gf)) → new_esEs6(yu300, yu411000, ge, gf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs4(yu30, yu41100, app(ty_Maybe, ed)) → new_esEs7(yu30, yu41100, ed)
new_esEs27(yu300, yu411000, app(app(app(ty_@3, bgd), bge), bgf)) → new_esEs11(yu300, yu411000, bgd, bge, bgf)
new_esEs18(:%(yu300, yu301), :%(yu411000, yu411001), fc) → new_asAs(new_esEs25(yu300, yu411000, fc), new_esEs26(yu301, yu411001, fc))
new_esEs5(yu31, yu41101, app(ty_Ratio, bdd)) → new_esEs18(yu31, yu41101, bdd)
new_esEs4(yu30, yu41100, app(ty_Ratio, fc)) → new_esEs18(yu30, yu41100, fc)
new_esEs21(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(app(ty_@3, dc), dd), de)) → new_esEs11(yu300, yu411000, dc, dd, de)
new_esEs5(yu31, yu41101, ty_Double) → new_esEs9(yu31, yu41101)
new_esEs6(Left(yu300), Left(yu411000), app(app(ty_Either, cf), cg), bf) → new_esEs6(yu300, yu411000, cf, cg)
new_esEs5(yu31, yu41101, app(app(ty_Either, bde), bdf)) → new_esEs6(yu31, yu41101, bde, bdf)
new_esEs24(yu301, yu411001, ty_Double) → new_esEs9(yu301, yu411001)
new_esEs27(yu300, yu411000, app(ty_[], bgg)) → new_esEs15(yu300, yu411000, bgg)
new_primPlusNat0(Zero, yu41100100) → Succ(yu41100100)
new_esEs23(yu300, yu411000, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs11(yu300, yu411000, bdh, bea, beb)
new_esEs23(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs12(EQ, GT) → False
new_esEs12(GT, EQ) → False
new_esEs4(yu30, yu41100, ty_Ordering) → new_esEs12(yu30, yu41100)
new_esEs4(yu30, yu41100, app(app(app(ty_@3, ee), ef), eg)) → new_esEs11(yu30, yu41100, ee, ef, eg)
new_esEs21(yu301, yu411001, app(ty_[], bae)) → new_esEs15(yu301, yu411001, bae)
new_esEs4(yu30, yu41100, app(ty_[], eh)) → new_esEs15(yu30, yu41100, eh)
new_esEs24(yu301, yu411001, app(app(ty_Either, bga), bgb)) → new_esEs6(yu301, yu411001, bga, bgb)
new_esEs24(yu301, yu411001, ty_@0) → new_esEs19(yu301, yu411001)
new_sr(Neg(yu3010), Pos(yu4110010)) → Neg(new_primMulNat0(yu3010, yu4110010))
new_sr(Pos(yu3010), Neg(yu4110010)) → Neg(new_primMulNat0(yu3010, yu4110010))
new_esEs24(yu301, yu411001, ty_Float) → new_esEs17(yu301, yu411001)
new_esEs24(yu301, yu411001, ty_Bool) → new_esEs13(yu301, yu411001)
new_esEs16(@2(yu300, yu301), @2(yu411000, yu411001), fa, fb) → new_asAs(new_esEs23(yu300, yu411000, fa), new_esEs24(yu301, yu411001, fb))
new_esEs6(Left(yu300), Left(yu411000), ty_Bool, bf) → new_esEs13(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs12(LT, GT) → False
new_esEs12(GT, LT) → False
new_esEs27(yu300, yu411000, app(app(ty_Either, bhc), bhd)) → new_esEs6(yu300, yu411000, bhc, bhd)
new_esEs20(yu300, yu411000, app(app(app(ty_@3, gh), ha), hb)) → new_esEs11(yu300, yu411000, gh, ha, hb)
new_esEs21(yu301, yu411001, app(ty_Maybe, baa)) → new_esEs7(yu301, yu411001, baa)
new_esEs20(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs21(yu301, yu411001, app(app(ty_Either, bba), bbb)) → new_esEs6(yu301, yu411001, bba, bbb)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs7(Just(yu300), Just(yu411000), ty_Int) → new_esEs8(yu300, yu411000)
new_esEs4(yu30, yu41100, ty_Float) → new_esEs17(yu30, yu41100)
new_esEs20(yu300, yu411000, app(app(ty_@2, hd), he)) → new_esEs16(yu300, yu411000, hd, he)
new_esEs26(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs17(Float(yu300, yu301), Float(yu411000, yu411001)) → new_esEs8(new_sr(yu300, yu411000), new_sr(yu301, yu411001))
new_esEs23(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Char) → new_esEs10(yu301, yu411001)
new_esEs5(yu31, yu41101, ty_Integer) → new_esEs14(yu31, yu41101)
new_esEs22(yu302, yu411002, app(ty_Ratio, bcb)) → new_esEs18(yu302, yu411002, bcb)
new_primEqNat0(Zero, Succ(yu4110000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu302, yu411002, ty_Float) → new_esEs17(yu302, yu411002)
new_esEs22(yu302, yu411002, ty_Ordering) → new_esEs12(yu302, yu411002)
new_esEs5(yu31, yu41101, ty_Char) → new_esEs10(yu31, yu41101)
new_esEs5(yu31, yu41101, app(ty_Maybe, bce)) → new_esEs7(yu31, yu41101, bce)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu411000, app(ty_Ratio, bef)) → new_esEs18(yu300, yu411000, bef)
new_esEs23(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs26(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs20(yu300, yu411000, app(app(ty_Either, hg), hh)) → new_esEs6(yu300, yu411000, hg, hh)
new_esEs5(yu31, yu41101, ty_Ordering) → new_esEs12(yu31, yu41101)
new_esEs7(Just(yu300), Just(yu411000), app(app(ty_@2, gb), gc)) → new_esEs16(yu300, yu411000, gb, gc)
new_esEs27(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Bool) → new_esEs13(yu31, yu41101)
new_esEs24(yu301, yu411001, app(ty_Maybe, bfa)) → new_esEs7(yu301, yu411001, bfa)
new_esEs23(yu300, yu411000, app(ty_Maybe, bdg)) → new_esEs7(yu300, yu411000, bdg)
new_esEs22(yu302, yu411002, app(ty_[], bbg)) → new_esEs15(yu302, yu411002, bbg)
new_esEs6(Left(yu300), Left(yu411000), app(ty_Maybe, be), bf) → new_esEs7(yu300, yu411000, be)
new_esEs25(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_Ordering, bf) → new_esEs12(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_@0, bf) → new_esEs19(yu300, yu411000)
new_esEs14(Integer(yu300), Integer(yu411000)) → new_primEqInt(yu300, yu411000)
new_esEs20(yu300, yu411000, app(ty_Ratio, hf)) → new_esEs18(yu300, yu411000, hf)
new_esEs6(Left(yu300), Left(yu411000), ty_Integer, bf) → new_esEs14(yu300, yu411000)
new_esEs11(@3(yu300, yu301, yu302), @3(yu411000, yu411001, yu411002), ee, ef, eg) → new_asAs(new_esEs20(yu300, yu411000, ee), new_asAs(new_esEs21(yu301, yu411001, ef), new_esEs22(yu302, yu411002, eg)))
new_esEs15([], :(yu411000, yu411001), eh) → False
new_esEs15(:(yu300, yu301), [], eh) → False
new_esEs4(yu30, yu41100, ty_Integer) → new_esEs14(yu30, yu41100)
new_esEs7(Just(yu300), Just(yu411000), app(ty_Ratio, gd)) → new_esEs18(yu300, yu411000, gd)
new_esEs6(Left(yu300), Left(yu411000), ty_Double, bf) → new_esEs9(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Int) → new_esEs8(yu31, yu41101)
new_esEs5(yu31, yu41101, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs11(yu31, yu41101, bcf, bcg, bch)
new_esEs6(Left(yu300), Right(yu411000), da, bf) → False
new_esEs6(Right(yu300), Left(yu411000), da, bf) → False
new_esEs21(yu301, yu411001, ty_Double) → new_esEs9(yu301, yu411001)
new_esEs21(yu301, yu411001, app(app(ty_@2, baf), bag)) → new_esEs16(yu301, yu411001, baf, bag)
new_sr(Neg(yu3010), Neg(yu4110010)) → Pos(new_primMulNat0(yu3010, yu4110010))
new_esEs12(LT, LT) → True
new_asAs(False, yu103) → False
new_sr(Pos(yu3010), Pos(yu4110010)) → Pos(new_primMulNat0(yu3010, yu4110010))
new_primEqNat0(Zero, Zero) → True
new_esEs27(yu300, yu411000, app(app(ty_@2, bgh), bha)) → new_esEs16(yu300, yu411000, bgh, bha)
new_esEs7(Just(yu300), Just(yu411000), ty_Float) → new_esEs17(yu300, yu411000)
new_primMulNat0(Zero, Succ(yu41100100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs4(yu30, yu41100, ty_@0) → new_esEs19(yu30, yu41100)
new_esEs4(yu30, yu41100, ty_Int) → new_esEs8(yu30, yu41100)
new_esEs23(yu300, yu411000, app(app(ty_Either, beg), beh)) → new_esEs6(yu300, yu411000, beg, beh)
new_esEs27(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Bool) → new_esEs13(yu301, yu411001)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_Ratio, ea)) → new_esEs18(yu300, yu411000, ea)
new_esEs23(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs15(:(yu300, yu301), :(yu411000, yu411001), eh) → new_asAs(new_esEs27(yu300, yu411000, eh), new_esEs15(yu301, yu411001, eh))
new_esEs20(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(ty_Either, eb), ec)) → new_esEs6(yu300, yu411000, eb, ec)
new_esEs24(yu301, yu411001, ty_Char) → new_esEs10(yu301, yu411001)
new_esEs22(yu302, yu411002, ty_Char) → new_esEs10(yu302, yu411002)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_[], df)) → new_esEs15(yu300, yu411000, df)
new_esEs4(yu30, yu41100, ty_Double) → new_esEs9(yu30, yu41100)
new_esEs13(False, False) → True
new_esEs20(yu300, yu411000, app(ty_[], hc)) → new_esEs15(yu300, yu411000, hc)
new_esEs23(yu300, yu411000, app(ty_[], bec)) → new_esEs15(yu300, yu411000, bec)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs4(yu30, yu41100, ty_Bool) → new_esEs13(yu30, yu41100)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs22(yu302, yu411002, ty_Double) → new_esEs9(yu302, yu411002)
new_esEs9(Double(yu300, yu301), Double(yu411000, yu411001)) → new_esEs8(new_sr(yu300, yu411000), new_sr(yu301, yu411001))
new_esEs4(yu30, yu41100, app(app(ty_Either, da), bf)) → new_esEs6(yu30, yu41100, da, bf)
new_esEs22(yu302, yu411002, ty_Int) → new_esEs8(yu302, yu411002)
new_primPlusNat0(Succ(yu1040), yu41100100) → Succ(Succ(new_primPlusNat1(yu1040, yu41100100)))
new_esEs27(yu300, yu411000, ty_Char) → new_esEs10(yu300, yu411000)
new_esEs20(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs24(yu301, yu411001, ty_Integer) → new_esEs14(yu301, yu411001)
new_esEs6(Left(yu300), Left(yu411000), ty_Int, bf) → new_esEs8(yu300, yu411000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu4110000))) → new_primEqNat0(yu3000, yu4110000)
new_esEs20(yu300, yu411000, ty_Float) → new_esEs17(yu300, yu411000)
new_esEs5(yu31, yu41101, ty_Float) → new_esEs17(yu31, yu41101)
new_esEs7(Just(yu300), Just(yu411000), ty_@0) → new_esEs19(yu300, yu411000)
new_esEs27(yu300, yu411000, ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs5(yu31, yu41101, app(app(ty_@2, bdb), bdc)) → new_esEs16(yu31, yu41101, bdb, bdc)
new_primPlusNat1(Zero, Succ(yu411001000)) → Succ(yu411001000)
new_primPlusNat1(Succ(yu10400), Zero) → Succ(yu10400)
new_esEs23(yu300, yu411000, app(app(ty_@2, bed), bee)) → new_esEs16(yu300, yu411000, bed, bee)
new_esEs20(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs12(LT, EQ) → False
new_esEs12(EQ, LT) → False
new_esEs27(yu300, yu411000, ty_Ordering) → new_esEs12(yu300, yu411000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs22(yu302, yu411002, app(app(ty_Either, bcc), bcd)) → new_esEs6(yu302, yu411002, bcc, bcd)
new_esEs6(Right(yu300), Right(yu411000), da, app(app(ty_@2, dg), dh)) → new_esEs16(yu300, yu411000, dg, dh)
new_esEs12(GT, GT) → True
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu4110000))) → False
new_esEs6(Right(yu300), Right(yu411000), da, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), ty_Char, bf) → new_esEs10(yu300, yu411000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(yu301, yu411001, ty_Float) → new_esEs17(yu301, yu411001)
new_esEs20(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_esEs19(@0, @0) → True
new_esEs27(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs20(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_asAs(True, yu103) → yu103
new_esEs23(yu300, yu411000, ty_Integer) → new_esEs14(yu300, yu411000)
new_esEs6(Left(yu300), Left(yu411000), app(ty_Ratio, ce), bf) → new_esEs18(yu300, yu411000, ce)
new_primMulNat0(Succ(yu30100), Succ(yu41100100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu41100100)), yu41100100)
new_esEs20(yu300, yu411000, ty_Double) → new_esEs9(yu300, yu411000)
new_esEs13(True, True) → True
new_esEs22(yu302, yu411002, ty_@0) → new_esEs19(yu302, yu411002)
new_esEs7(Just(yu300), Just(yu411000), app(app(app(ty_@3, ff), fg), fh)) → new_esEs11(yu300, yu411000, ff, fg, fh)
new_esEs7(Just(yu300), Just(yu411000), ty_Char) → new_esEs10(yu300, yu411000)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu4110000))) → new_primEqNat0(yu3000, yu4110000)
new_esEs22(yu302, yu411002, ty_Bool) → new_esEs13(yu302, yu411002)
new_esEs22(yu302, yu411002, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs11(yu302, yu411002, bbd, bbe, bbf)
new_esEs6(Left(yu300), Left(yu411000), ty_Float, bf) → new_esEs17(yu300, yu411000)
new_esEs24(yu301, yu411001, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs11(yu301, yu411001, bfb, bfc, bfd)
new_esEs5(yu31, yu41101, app(ty_[], bda)) → new_esEs15(yu31, yu41101, bda)
new_esEs4(yu30, yu41100, app(app(ty_@2, fa), fb)) → new_esEs16(yu30, yu41100, fa, fb)
new_primEqNat0(Succ(yu3000), Succ(yu4110000)) → new_primEqNat0(yu3000, yu4110000)
new_esEs4(yu30, yu41100, ty_Char) → new_esEs10(yu30, yu41100)
new_esEs7(Just(yu300), Just(yu411000), ty_Bool) → new_esEs13(yu300, yu411000)
new_esEs24(yu301, yu411001, app(ty_Ratio, bfh)) → new_esEs18(yu301, yu411001, bfh)
new_esEs6(Right(yu300), Right(yu411000), da, ty_Ordering) → new_esEs12(yu300, yu411000)
new_esEs21(yu301, yu411001, app(app(app(ty_@3, bab), bac), bad)) → new_esEs11(yu301, yu411001, bab, bac, bad)
new_esEs6(Left(yu300), Left(yu411000), app(app(app(ty_@3, bg), bh), ca), bf) → new_esEs11(yu300, yu411000, bg, bh, ca)
new_esEs12(EQ, EQ) → True
new_esEs7(Nothing, Nothing, ed) → True
new_esEs24(yu301, yu411001, app(ty_[], bfe)) → new_esEs15(yu301, yu411001, bfe)
new_esEs23(yu300, yu411000, ty_Int) → new_esEs8(yu300, yu411000)
new_esEs21(yu301, yu411001, ty_Int) → new_esEs8(yu301, yu411001)
new_esEs15([], [], eh) → True
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu4110000))) → False
new_esEs27(yu300, yu411000, ty_@0) → new_esEs19(yu300, yu411000)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs22(yu302, yu411002, app(ty_Maybe, bbc)) → new_esEs7(yu302, yu411002, bbc)
new_esEs21(yu301, yu411001, app(ty_Ratio, bah)) → new_esEs18(yu301, yu411001, bah)
new_esEs8(yu30, yu41100) → new_primEqInt(yu30, yu41100)
new_esEs6(Right(yu300), Right(yu411000), da, app(ty_Maybe, db)) → new_esEs7(yu300, yu411000, db)
The set Q consists of the following terms:
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_sr(Neg(x0), Neg(x1))
new_esEs20(x0, x1, ty_Bool)
new_esEs7(Just(x0), Just(x1), ty_Int)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Int)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs21(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs20(x0, x1, ty_Integer)
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, ty_Double)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs24(x0, x1, ty_Double)
new_esEs22(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_esEs15(:(x0, x1), [], x2)
new_esEs4(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_asAs(True, x0)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs12(GT, EQ)
new_esEs12(EQ, GT)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs20(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs5(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(GT, GT)
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Double)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Float)
new_esEs14(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs8(x0, x1)
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat0(Succ(x0), x1)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs7(Just(x0), Just(x1), ty_Char)
new_esEs7(Nothing, Nothing, x0)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Ordering)
new_esEs7(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Zero)
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs13(False, False)
new_esEs5(x0, x1, ty_Int)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs7(Just(x0), Just(x1), ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_esEs13(False, True)
new_esEs13(True, False)
new_esEs5(x0, x1, ty_Char)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Just(x0), Just(x1), ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs7(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs15([], [], x0)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs4(x0, x1, ty_Char)
new_esEs7(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs4(x0, x1, ty_Int)
new_esEs13(True, True)
new_esEs7(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs15([], :(x0, x1), x2)
new_esEs27(x0, x1, ty_Integer)
new_esEs7(Nothing, Just(x0), x1)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(:(x0, x1), :(x2, x3), x4)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs21(x0, x1, ty_Bool)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs23(x0, x1, ty_Bool)
new_esEs7(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(EQ, LT)
new_esEs12(LT, EQ)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs7(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Int)
new_esEs12(EQ, EQ)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(Just(x0), Nothing, x1)
new_primPlusNat0(Zero, x0)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(Char(x0), Char(x1))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Ordering)
new_esEs7(Just(x0), Just(x1), ty_Double)
new_esEs19(@0, @0)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs26(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Double)
new_esEs20(x0, x1, ty_Char)
new_esEs12(LT, LT)
new_esEs24(x0, x1, ty_Int)
new_esEs12(LT, GT)
new_esEs12(GT, LT)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs21(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(yu85, False, yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)
The graph contains the following edges 5 > 2, 5 > 3, 7 >= 6, 8 >= 7
- new_psPs(yu85, True, yu87, yu88, yu89, yu90, ba, bb) → new_psPs0(yu87, yu88, yu89, yu90, ba, bb)
The graph contains the following edges 3 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5, 8 >= 6
- new_psPs0(yu87, yu88, :(yu890, yu891), yu90, ba, bb) → new_foldr(@2(yu87, yu88), yu890, yu891, new_primPlusNat0(yu90, Zero), new_primPlusNat0(yu90, Zero), ba, bb)
The graph contains the following edges 3 > 2, 3 > 3, 5 >= 6, 6 >= 7
- new_foldr(@2(yu30, yu31), @2(yu41100, yu41101), yu4111, yu61, yu62, bc, bd) → new_psPs(yu61, new_asAs(new_esEs4(yu30, yu41100, bc), new_esEs5(yu31, yu41101, bd)), yu30, yu31, yu4111, yu62, bc, bd)
The graph contains the following edges 4 >= 1, 1 > 3, 1 > 4, 3 >= 5, 5 >= 6, 6 >= 7, 7 >= 8